<p>
The field is marked as nonnull, but isn't written to by the constructor.
The field might be initialized elsewhere during constructor, or might always
be initialized before use.
</p>
